Nuprl Lemma : weak-antecedent-surjections-compose 11,40
es:ES, P, Q, R:(E), f:({e:E| P(e)} {e:E| Q(e)} ), g:({e:E| Q(e)} {e:E| R(e)} ).
(Q = f== P & R = g== Q)  R = g o f== P 
latex

Definitionst  T, x:A. B(x), Q = f== P, x:A  B(x), , P & Q, P  Q, E, f(a), {x:A| B(x)} , x:AB(x), Type, ES, Q ==f== P, s = t, x:A. B(x), A c B, f o g
Lemmasmember wf, compose wf, es-E wf, weak-antecedent-functions-compose, weak-antecedent-surjection wf

origin